Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    a__primes  → a__sieve(a__from(s(s(0))))
2:    a__from(X)  → cons(mark(X),from(s(X)))
3:    a__head(cons(X,Y))  → mark(X)
4:    a__tail(cons(X,Y))  → mark(Y)
5:    a__if(true,X,Y)  → mark(X)
6:    a__if(false,X,Y)  → mark(Y)
7:    a__filter(s(s(X)),cons(Y,Z))  → a__if(divides(s(s(mark(X))),mark(Y)),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))
8:    a__sieve(cons(X,Y))  → cons(mark(X),filter(X,sieve(Y)))
9:    mark(primes)  → a__primes
10:    mark(sieve(X))  → a__sieve(mark(X))
11:    mark(from(X))  → a__from(mark(X))
12:    mark(head(X))  → a__head(mark(X))
13:    mark(tail(X))  → a__tail(mark(X))
14:    mark(if(X1,X2,X3))  → a__if(mark(X1),X2,X3)
15:    mark(filter(X1,X2))  → a__filter(mark(X1),mark(X2))
16:    mark(s(X))  → s(mark(X))
17:    mark(0)  → 0
18:    mark(cons(X1,X2))  → cons(mark(X1),X2)
19:    mark(true)  → true
20:    mark(false)  → false
21:    mark(divides(X1,X2))  → divides(mark(X1),mark(X2))
22:    a__primes  → primes
23:    a__sieve(X)  → sieve(X)
24:    a__from(X)  → from(X)
25:    a__head(X)  → head(X)
26:    a__tail(X)  → tail(X)
27:    a__if(X1,X2,X3)  → if(X1,X2,X3)
28:    a__filter(X1,X2)  → filter(X1,X2)
There are 29 dependency pairs:
29:    A__PRIMES  → A__SIEVE(a__from(s(s(0))))
30:    A__PRIMES  → A__FROM(s(s(0)))
31:    A__FROM(X)  → MARK(X)
32:    A__HEAD(cons(X,Y))  → MARK(X)
33:    A__TAIL(cons(X,Y))  → MARK(Y)
34:    A__IF(true,X,Y)  → MARK(X)
35:    A__IF(false,X,Y)  → MARK(Y)
36:    A__FILTER(s(s(X)),cons(Y,Z))  → A__IF(divides(s(s(mark(X))),mark(Y)),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))
37:    A__FILTER(s(s(X)),cons(Y,Z))  → MARK(X)
38:    A__FILTER(s(s(X)),cons(Y,Z))  → MARK(Y)
39:    A__SIEVE(cons(X,Y))  → MARK(X)
40:    MARK(primes)  → A__PRIMES
41:    MARK(sieve(X))  → A__SIEVE(mark(X))
42:    MARK(sieve(X))  → MARK(X)
43:    MARK(from(X))  → A__FROM(mark(X))
44:    MARK(from(X))  → MARK(X)
45:    MARK(head(X))  → A__HEAD(mark(X))
46:    MARK(head(X))  → MARK(X)
47:    MARK(tail(X))  → A__TAIL(mark(X))
48:    MARK(tail(X))  → MARK(X)
49:    MARK(if(X1,X2,X3))  → A__IF(mark(X1),X2,X3)
50:    MARK(if(X1,X2,X3))  → MARK(X1)
51:    MARK(filter(X1,X2))  → A__FILTER(mark(X1),mark(X2))
52:    MARK(filter(X1,X2))  → MARK(X1)
53:    MARK(filter(X1,X2))  → MARK(X2)
54:    MARK(s(X))  → MARK(X)
55:    MARK(cons(X1,X2))  → MARK(X1)
56:    MARK(divides(X1,X2))  → MARK(X1)
57:    MARK(divides(X1,X2))  → MARK(X2)
The approximated dependency graph contains one SCC: {29-35,37-57}.
Tyrolean Termination Tool  (94.88 seconds)   ---  May 3, 2006